kpr |= X == s:Sem. K-sem(S;equiv)(kpr,s)  X(s) 

latex

---

clarification:

K-sem-sat(Sem;equiv;S;kpr;X) == s:Sem. K-sem(S;equiv)(kpr,s)  X(s) 

latex

Definitions	x:A. B(x), P  Q, K-sem(S;equiv)
FDL editor aliases	K-sem-sat